COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	We work within
C00010 ENDMK
C⊗;
We work within
first order logic, so that
%2Value AAll(XX1,CChild(MMike,XX1) IImplies KKnow(MMike,TTelephone XX1))%1
which is the proposition that Mike knows the telephone numbers of all his
children, is formed by applying the function ⊗AAll to two arguments which
in turn are built up from their elementary constituents.
We start with a two classes of ⊗objects,
%2inner variables%1 and ⊗constants, and build up from them
the class of %2abstract forms%1 using certain functions
with names like ⊗ttelephone and ⊗TTelephone.

	As far as the (outer) logic is concerned the %2inner variables%1
are objects and not variables at all, and therefore we will need
variables that can take inner variables as values.  Moreover, %2inner
variables%1 can either range over concepts or things.  To keep all this
straight we make the following typographical conventions:

1. As before,  an expression whose value is a concept begins in upper case and
one whose value is a thing is in lower case.  We distinguish abstract forms
having concepts or things as values from the concepts or things by doubling
the initial letters.  Therefore, alas, we have ⊗mike, ⊗Mike, ⊗mmike
and ⊗MMike, the last two being abstract forms.  It may later be possible
to get rid of ⊗MMike. 

2. An %2inner variable%1 is represented by a doubled letter followed
by digits, and a variable ranging over %2abstract forms%1 is represented
by doubled letters without digits.  Thus  ⊗XX0 is an inner variable
ranging over concepts, and ⊗XX is a variable ranging over concept-valued
abstract forms which will include inner variables like ⊗XX0. 
Likewise ⊗xx0 is an inner variable representing things, and
⊗xx is a variable ranging thing-valued abstract forms.

	Inner variables are one kind of abstract form, and another kind
are constants.  Constants are treated similarly to variables.  Thus
we have ⊗MMike - a ⊗constant whose value is the concept represented
by ⊗Mike, and ⊗mmike a constant whose value is ⊗mike himself.

	Abstract forms are built from constants and variables by
functions.  Thus ⊗TTelephone takes an abstract form representing a
person into an abstract form representing his telephone number.
Thus we have %2TTelephone PP0%1 is an abstract form and so is
%2TTelephone MMike%1.  %2TTelephone PP%1 is an expression with a variable
⊗PP ranging over abstract forms.
Corresponding to all the functions of the previous sections we have
form-making functions represented by doubling the initial letters.

	We have two additional ways of making abstract forms.  Namely,
if ⊗XX is an inner variable and ⊗QQ is an abstract form, then
⊗AAll(XX,QQ) is an abstract form and so is ⊗TThe(XX,QQ).
Thus %2TThe(PP0,KKnow(PP0,TTelephone MMike))%1 is an abstract form,
and we intend that it shall have as value a concept of the unique
person who knows Mike's telephone number.  In the logic ⊗AAll and
⊗TThe are functions.  In order to avoid trouble with bound variables,
we shall want

!!g50:	%2TThe(PP0,KKnow(PP0,TTelephone MMike)) = TThe(PP5,KKnow(PP5,TTelephone Mike))%1
i.e. the abstract form produced by ⊗AAll is invariant under alphabetic
change of bound variable.  This is part of the reason for calling them
⊗abstract. 


	In order to go from concept-valued abstract forms to concepts,
we introduce two functions %2Value EE%1 and %2Value(EE,π)%1 where π
is called a state vector and assigns values to all inner variables.
If the abstract form ⊗EE has no inner variables, then %2Value EE%1
can be used.  The inner form %2TThe(PP0,KKnow(PP0,TTelephone MMike))%1
has no variables; the function ⊗TThe gets rid of the variable ⊗PP0 
in its second argument, so %2Value TThe(PP0,KKnow(PP0,TTelephone MMike))%1
is the concept of the unique person who knows Mike's telephone number.
If there is such a person, then
%2denote Value TThe(PP0,KKnow(PP0,TTelephone MMike))%1 is that person.

	Similarly,

!!g51:	%2Value AAll(PP0,KKnow(PP0,TTelephone MMike) Implies
KKnow(PP0,TTelephone MMary))%1

is the proposition that everyone who knows Mike's telephone number
also knows Mary's.

(If the reader is getting impatient with all this formalism, let him
remember that the above formulas are constants in a first order logic
formalism, i.e. are formed by applying functions to arguments.  This
will pay off later, I promise).

	Actually, we may have made more distinctions in the notation
than are necessary, but it is easier to remove them than add them later.